<!DOCTYPE html>

<html>

<head>
  <meta charset="utf-8" />
  <meta name="keywords" content="remark,remarkjs,markdown,slideshow,presentation" />
  <meta name="description" content="A simple, in-browser, markdown-driven slideshow tool." />
  <link rel="stylesheet" href="./styles/style.css">
  <title>Remark</title>
</head>

<body>
  <textarea id="source">
    name: inverse
    layout: true
    class: inverse
    ---
    # Assertion Based Verification (ABV)

    Yue Tao
    
    Institute of Software, CAS

    ---

    ```scala

      // Formal Verification
      when (past(feedback.valid) && isBranch(past(feedback.operType))){
    
        val memReadPrev = mem.read(addr.getIdx(past(feedback.pc)))
        
        when (past(feedback).branchTaken) {
          when (past(currCount) =/= "b11".U) {
            assert(memReadPrev === past(currCount) + 1.U)
          }.otherwise {
            assert(memReadPrev === "b11".U)
          }
        }.otherwise {
          when (past(currCount) =/= "b00".U) {
            assert(memReadPrev === past(currCount) - 1.U)
          }.otherwise {
            assert(memReadPrev === "b00".U)
          }
        }
      }
    
    }
    
    ```

    ---

    # Signal & Property

    ```scala
    assert(memReadPrev === past(currCount) + 1.U)
    ```

    - **Signal**: Port / Wire / etc.

    - **Property**: logic expressions.

    ---

    # Verify with Assertions

    - No value specified. Verification tools enumerate **ALL** possible values.

    - FAIL when combination of signal values found violating assertion. 

    - Make assertions stand & reduce search space by specifying conditions & assumptions.

    ---

    # Differs from Testing

    .left[
    - Testing: separates DUT and Test Bench<br>
      Assertion: intertwine with code

    - Testing: uses limited cases (stimulus)<br>
      Assertion: enumerates ALL cases

    - **Testing: uses implemented model**<br>
      **Assertion: builds another model**
    ]

    ---
    
      ![:scale 100%](./assets/state.png)

    ---

    # Difficulties with Writing Assertions

    - You just don't know how to write assertions that **REALLY** verify the model.

      - Not too simple (or it verifies nothing)

      - Not too detailed (or the solver gets stuck)

      - Not too careless (or you'll get lost)


    ---

    # Write Assertions in Practice

    - Confirm with the pattern <br>(FSM / Memory / Async / Combo / etc.)

    - Starting from **tautology**

    - Replace signals, and conditions gradually

    - Find contradictory between spec. & impl. .

    ---


    # Advices

    - Employ Assertions & Formal Verification ASAP.

    - Break down the "Stages" or "Function Units" into small verifiable components.

    ---

    # Refs:

    [1] [Verilog Formal Verification Tutorial, Gisselquist](https://zipcpu.com/tutorial/class-verilog.pdf) 

    [2] [Formal Verification with Chisel, Laeufer](https://woset-workshop.github.io/PDFs/2021/a03-slides.pdf)

  </textarea>

  <script src="./js/remark-latest.min.js"></script>
  <script>
    var hljs = remark.highlighter.engine;
  </script>
  <!-- <script src="remark.language.js"></script> -->
  <script>

    remark.macros.scale = function (percentage) {
      var url = this;
      return '<img src="' + url + '" style="width: ' + percentage + '" />';
    };

    var slideshow = remark.create({
      highlightStyle: 'monokai',
      highlightLanguage: 'remark',
      highlightLines: true
    });
  </script>

</html>
